(set-logic QF_BV)
(declare-fun x () (_ BitVec 5))
(declare-fun y () (_ BitVec 4))
(assert
  (let ((e3 (bvsrem ((_ sign_extend 1) y) x)))
  (let ((e4 (bvsub e3 (_ bv0 5))))
  (let ((e5 (bvugt e3 ((_ zero_extend 1) y))))
  (let ((e8 (bvuge x e4)))
  (let ((e11 (ite e5 e5 e8)))
  (let ((e14 (=> e11 false)))
  (let ((e16 (and e14 e14)))
  (let ((e17 e16))
  (let ((e18 (and e17 (not (= x (_ bv0 5))))))
  (let ((e19 e18)) e19)))))))))))
(check-sat)
